『Mathematics in Lean』

メモ

1章

table:訳

英語 日本語

tactic 戦術、タクティク

identity 同一

rw: 書き換えタクティク

mul_comm a b

可換則

a * b = b * a

mul_assoc a b c

結合則

a * b * c = a * (b * c)

ここで暗黙的にa * b * cは(a * b) * cになっている

code:lean

example (a b c : ℝ) : a * b * c = b * (a * c) := by

3章

rcases

7章

7. Hierarchies

7.1. Basics

7.2. Morphisms

7.3. Sub-objects

オブジェクト指向の方でもよく出るやつ

Leanの開発中に同じような問題に遭遇したとのこと